Coq マクロ
#Fleeting_Notes
Coq マクロ(Coq macro)
言語的な制約でイケてないほうのマクロの例
math-comp/boot/bigop.v at 7774a951d10d8369b8816422c7b2dacc765457b2 · math-comp/math-comp
確認用
Q. Coq マクロ
メモ
『Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages』
調査用
Google.icon
Coq マクロ(日)
Google.icon
Coq macro(英)